Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-14 23:35:49)
• ✅ Mathlib branch lean-pr-testing-6083 has successfully built against this PR. (2024-11-21 08:55:45) View Log
• ✅ Mathlib branch lean-pr-testing-6083 has successfully built against this PR. (2024-11-26 07:13:12) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 827062f807cd869709fb71d5d04a00ff10320be3 --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 01:12:55)

Is there any advantage of using abbrev over theorem in this case?

Is there any advantage of using abbrev over theorem in this case?

Yes, we can use abbrev X := @Y, to avoid having the type out the signature, when deprecating. In Batteries and below, we have alias, but I don't think alias is ready to move upstream (precisely because it results in us having too many ways to do the same thing: eventually I would like a unification of abbrev and alias functionality into a single keyword).

I'm adding the awaiting-review tag as I would like another set of eyes on this before merging. It feels a bit hacky to me still. :-(

This is an intermediate measure until we decide on a unification of alias / abbrev etc.